HOL Light - kt3k cosense

HOL Light

HOL 系の Theorem prover

by John Harrison

HOL の最初のバージョンを作った Mike Gordon は John Harrison の先生

GitHub https://github.com/jrh13/hol-light/

HOL Light ホームページ

https://www.cl.cam.ac.uk/~jrh13/hol-light/index.html

HOL Light チュートリアル

https://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf

HOL Light は OCaml の内部 DSL として書かれている

#Math #数学基礎論 #Proof_assistant